es:ES, X:AbsInterface(Top), e:E. ((e  le(X)))  le(X)(e) c e 

latex

Definitions

t  T, b, E, e loc e' , s = t, x:AB(x), x:A. B(x), AbsInterface(A), a:A fp B(a), E(X), Top, le(X), strong-subtype(A;B), P  Q, ES, left + right, X(e), e  X, P  Q, (e <loc e'), x:A  B(x), let x,y = A in B(x;y), t.1, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , Type, EqDecider(T), Unit, IdLnk, Id, EOrderAxioms(E; pred?; info), f(a), EState(T), Knd, x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , constant_function(f;A;B), P & Q, e c e', (e < e'), {x:A| B(x)} ,

Lemmas

es-interface-subtype rel, es-E-interface-subtype rel, es-le-interface-le, es-causle wf, es-is-interface wf, es-causle weakening locl, es-interface-val wf, constant function wf, assert wf, bool wf, qle wf, cless wf, val-axiom wf, rationals wf, nat wf, Msg wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, Id wf, IdLnk wf, unit wf, deq wf, event system wf, member wf, top wf, es-le-interface wf, es-E wf, es-E-interface wf, es-interface wf, subtype rel wf